This present disclosure relates generally to formal verification of circuit designs, and more particularly to formal verification methods of verifying data access and data propagation paths in multi-system circuits.
Devices such as mobile phones, gaming consoles, and set top boxes often include multiple computing devices that store, share, or otherwise access sensitive data. For example, sensitive data, such as encryption and decryption keys, may be designed to be read from secure locations within a computing device and sent to other secure functional components through secure channels within the device. Handling of sensitive data has related security requirements, which generally specify that (1) secure data and control information should not reach non-secure areas of the computing device and (2) non-secure data and control information should not propagate to secure areas of the computing device or interfere with secure operations performed by the computing device. The role of initiators (e.g., masters) and receivers (e.g., slaves) regarding one or a combination of data and control information are important when analyzing these requirements. Analysis regarding whether secure data and control information has passed through an encryption path or not is also important.
Overall, the process of integrating multiple intellectual property (IP) functional components to create multi-system circuits sometimes provides an unexpected path to secure areas of the computing device. The addition of test logic and associated test ports may create a path by which secure data may be accessed by an interface external to the computing device. The resulting path may create a security leak (i.e. violation to requirement 1 above) or an illegal modification or interference on a secure area (i.e. violation to requirement 2 above). Current techniques used to verify that a design is free from data security leaks or unintentional pathways creating unauthorized data access are insufficient.
Summary
Embodiments include a formal verification approach for verifying data access and data propagation paths in multi-system circuits by proving the unreachability of path cover properties of the circuit design. In one embodiment, a security path verification system receives an original circuit model of a circuit design. As used herein, the term “circuit model” may refer to a model of an entire circuit or any portion of a circuit. The security path verification system also receives parameters identifying a first location within the circuit design that is a source of tainted data and a second location within the circuit design that is coupled to the first location. To tune or optimize the formal verification process, the security path verification system may receive a selection of portions of the circuit design that include logic to be excluded from the verification analysis. Logic to be excluded is received by the security path verification system as an indication of a portion of the circuit design to be modeled as a black box, where the indicated portion is located along one more transmission paths between the first and second locations within the circuit design. Traditional analysis excludes the logic in the blackboxed module from the analysis and allows any arbitrary values at the outputs of such module. But to ensure that tainted data may still propagate through the excluded logic, the security path verification system replaces the excluded logic with a connectivity abstraction, intended to maintain the data propagation properties of the excluded logic. Traditional handling of blackboxed modules in formal verification of generic properties, in contrast, merely allows any arbitrary value to propagate to the outputs of the blackboxed module. The disclosed embodiments, however, use a functional representation of the blackboxed module, with not as much details as the actual circuit description of the module, but with details sufficient for security verification. The connectivity abstraction may be generated in netlist form or other appropriate representation. Using the connectivity abstraction, the security verification system generates a second circuit model of the circuit design by modifying the first circuit model with the abstracted version of the excluded portion of the circuit design. Using the second circuit model, the security verification system determines whether the tainted data can reach the second location within the circuit design from the first location within the circuit design. In one embodiment, formal verification may be used to verify whether the tainted data can reach the second location within the circuit design from the first location within the circuit design. By using a modified circuit model that includes the connectivity abstraction, the security verification system provides a tunable analysis environment that allows the propagation of tainted data. Furthermore, the security verification may involve restricting the analysis to only consider paths that go through or do not go through the specified signal paths. Accordingly, the disclosed embodiments yield verification results with a measurable level of completeness compared to other security path verification techniques.
For example, some security path verification techniques use structural analysis, which requires a user to manually trace of a path to verify the presence of a blocking agent. Such an approach is often impractical because of the tedious process of analyzing a very large number of potential paths. Moreover, structural analysis is often subjective, lacking a clear checking mechanism. Other security data path verification techniques use dynamic simulation methods, where user would generate different stimulus on the inputs of the system, simulating attacks done by a hacker. Yet, using this approach not all possible attacks can be covered by the engineer in reasonable time. Moreover, simulation tools currently available do not reliably detect if security requirements have been violated. These deficiencies increase the likelihood that security-related issues will not be discovered during the design/verification phase. And like structural analysis techniques, dynamic simulation methods also fail to yield to verification results with a measurable level of completeness.
The figures depict various embodiments of the present disclosure for purposes of illustration only. One skilled in the art will readily recognize from the following discussion that alternative embodiments of the structures and methods illustrated herein may be employed without departing from the principles of the embodiments described herein.